ds:x:Id fp Type, da:k:Knd fp Type, k:Knd, test:(State(ds)Valtype(da;k)).
ecl-base-tuple(k;test)  ecl-trans-tuple{i:l}(ds;da) 

latex

Definitions	t  T, x:A. B(x), Valtype(da;k), {T}, P  Q, SQType(T), Knd, Prop, State(ds), , p  q, P & Q, P  Q, b, A, b, Unit, (x  l), p  q, , , false, i=j, ecl-base-tuple(k;test), ecl-trans-tuple{i:l}(ds;da), Id, x. t(x), a:A fp B(a), a = b
Lemmas	fpf wf, Id wf, eq int wf, bfalse wf, nat wf, nat plus wf, band wf, l member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, eq knd wf, assert-eq-knd, bor wf, bool wf, decl-state wf, Knd wf, Knd sq, subtype rel self, ma-valtype wf